<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.0 Transitional//EN"
            "http://www.w3.org/TR/REC-html40/loose.dtd">
<HTML>
<HEAD>



<META http-equiv="Content-Type" content="text/html; charset=ISO-8859-1">
<META name="GENERATOR" content="hevea 1.08">
<LINK rel="stylesheet" type="text/css" href="libman.css">
<TITLE>
The CHR Language
</TITLE>
</HEAD>
<BODY >
<A HREF="libman045.html"><IMG SRC ="previous_motif.gif" ALT="Previous"></A>
<A HREF="libman042.html"><IMG SRC ="contents_motif.gif" ALT="Up"></A>
<A HREF="libman047.html"><IMG SRC ="next_motif.gif" ALT="Next"></A>
<HR>

<H2 CLASS="section"><A NAME="htoc83">8.4</A>&nbsp;&nbsp;The <FONT COLOR=purple>CHR</FONT> Language</H2><UL>
<LI><A HREF="libman046.html#toc39">Constraint Handling Rules</A>
<LI><A HREF="libman046.html#toc40">How <FONT COLOR=purple>CHR</FONT>s Work</A>
</UL>

User-defined constraints are defined by constraint handling rules
- and optional
ECL<SUP><I>i</I></SUP>PS<SUP><I>e</I></SUP> clauses for the built-in labeling feature.
The constraints must be declared before they are defined.
A <FONT COLOR=purple>CHR</FONT> program (file extension <TT>chr</TT>) may also include other declarations,
options and arbitrary ECL<SUP><I>i</I></SUP>PS<SUP><I>e</I></SUP> clauses.
<DIV CLASS="center">
<TABLE BORDER=1 CELLSPACING=0 CELLPADDING=1>
<TR><TD ALIGN=left NOWRAP>Program</TD>
<TD VALIGN=top ALIGN=center NOWRAP>&nbsp;::=&nbsp;</TD>
<TD ALIGN=left NOWRAP>Statement [ Program ]</TD>
</TR>
<TR><TD ALIGN=left NOWRAP>Statement</TD>
<TD VALIGN=top ALIGN=center NOWRAP>&nbsp;::=&nbsp;</TD>
<TD ALIGN=left NOWRAP>Declaration |&nbsp;Option |&nbsp;Rule |&nbsp;Clause</TD>
</TR></TABLE>
</DIV>
Constraint handling rules involving
the same constraint can be scattered across a file as long as they are
in the same module and compiled together. For readability
declarations and options should precede rules and clauses.<BR>
<BR>
In the following subsections, we introduce constraint handling
rules and explain how they work. The next section 
describes declarations, clauses, options 
and built-in predicates for <FONT COLOR=purple>CHR</FONT>s.<BR>
<BR>
<A NAME="toc39"></A>
<H3 CLASS="subsection"><A NAME="htoc84">8.4.1</A>&nbsp;&nbsp;Constraint Handling Rules</H3>
A constraint handling rule has one or two heads, an optional guard, a
body and an optional name. A &#8220;Head&#8221; is a &#8220;Constraint&#8221;. A
&#8220;Constraint&#8221; is an ECL<SUP><I>i</I></SUP>PS<SUP><I>e</I></SUP> <EM>callable term</EM> (i.e. atom or
structure) whose functor is a declared constraint. A
&#8220;Guard&#8221;<A NAME="@default232"></A> is an ECL<SUP><I>i</I></SUP>PS<SUP><I>e</I></SUP> goal. The <EM>guard is a test</EM>
on the applicability of a rule. The &#8220;Body&#8221; of a rule is an
ECL<SUP><I>i</I></SUP>PS<SUP><I>e</I></SUP> goal (including constraints). 
The execution of the guard and the body should not involve
side-effects (like <TT>assert/1</TT>, <TT>write/1</TT>) (for more information
see the section on writing <FONT COLOR=purple>CHR</FONT> programs). A rule can be named with
a &#8220;RuleName&#8221; which can be any ECL<SUP><I>i</I></SUP>PS<SUP><I>e</I></SUP> term (including variables
from the rule). During debugging (see section
<A HREF="libman050.html#chrdebug">8.8</A>),
this name will be displayed instead of the
whole rule.<BR>
<BR>
There are three kinds of constraint handling rules.
<DIV CLASS="center">
<TABLE BORDER=1 CELLSPACING=0 CELLPADDING=1>
<TR><TD ALIGN=left NOWRAP>Rule</TD>
<TD VALIGN=top ALIGN=center NOWRAP>&nbsp;::=&nbsp;</TD>
<TD ALIGN=left NOWRAP>SimplificationRule |&nbsp;PropagationRule |&nbsp;SimpagationRule</TD>
</TR>
<TR><TD ALIGN=left NOWRAP>SimplificationRule</TD>
<TD VALIGN=top ALIGN=center NOWRAP>&nbsp;::=&nbsp;</TD>
<TD ALIGN=left NOWRAP>[ RuleName <CODE>@</CODE> ] Head [ <CODE>,</CODE> Head ] <CODE> &lt;=&gt;</CODE> [Guard <CODE>|</CODE>] Body.</TD>
</TR>
<TR><TD ALIGN=left NOWRAP>PropagationRule</TD>
<TD VALIGN=top ALIGN=center NOWRAP>&nbsp;::=&nbsp;</TD>
<TD ALIGN=left NOWRAP>[ RuleName <CODE>@</CODE> ] Head [ <CODE>,</CODE> Head ] <CODE> ==&gt;</CODE> [Guard <CODE>|</CODE>] Body.</TD>
</TR>
<TR><TD ALIGN=left NOWRAP>SimpagationRule</TD>
<TD VALIGN=top ALIGN=center NOWRAP>&nbsp;::=&nbsp;</TD>
<TD ALIGN=left NOWRAP>[ RuleName <CODE>@</CODE> ] Head <CODE>\</CODE> Head <CODE> &lt;=&gt;</CODE> [Guard <CODE>|</CODE>] Body.</TD>
</TR></TABLE>
</DIV><BR>
<BR>
Declaratively, a rule relates heads and body <EM>provided the guard
is true</EM>. A simplification rule<A NAME="@default233"></A> means that
the heads are true if and only if the body is true. A propagation
rule<A NAME="@default234"></A> means that the body is true if the heads
are true. A simpagation rule<A NAME="@default235"></A> is a combination
of a simplification and propagation rule. The rule &#8220;Head1 <CODE>\</CODE>
Head2
<CODE>&lt;=&gt;</CODE> Body&#8221; is equivalent to the simplification rule
&#8220;Head1 <CODE>,</CODE> Head2 <CODE>&lt;=&gt;</CODE> Body<CODE>,</CODE> Head1<CODE>.</CODE>&#8221;
However, the simpagation rule is more compact to write, more efficient
to execute and has better termination behavior than the corresponding
simplification rule.<BR>
<BR>
<B>Example:</B>
Assume you want to write a constraint handler for minimum and maximum
based on inequality constraints. The complete code can be found in
the handler file <TT>minmax.chr</TT>. <PRE CLASS="verbatim"> handler minmax.

constraints leq/2, neq/2, minimum/3, maximum/3.
built_in     @ X leq Y &lt;=&gt; \+nonground(X),\+nonground(Y) | X @=&lt; Y.
reflexivity  @ X leq X &lt;=&gt; true.
antisymmetry @ X leq Y, Y leq X &lt;=&gt; X = Y.
transitivity @ X leq Y, Y leq Z ==&gt; X \== Y, Y \== Z, X \== Z | X leq Z.
...
built_in     @ X neq Y &lt;=&gt; X \== Y | true.
irreflexivity@ X neq X &lt;=&gt; fail. 
...
subsumption  @ X lss Y \ X neq Y &lt;=&gt; true.
simplification @ X neq Y, X leq Y &lt;=&gt; X lss Y. 
...
min_eq @ minimum(X, X, Y) &lt;=&gt; X = Y.
min_eq @ minimum(X, Y, X) &lt;=&gt; X leq Y.
min_eq @ minimum(X, Y, Y) &lt;=&gt; Y leq X.
...
propagation @ minimum(X, Y, Z) ==&gt; Z leq X, Z leq Y.
...
</PRE>
Procedurally, a rule can fire only if its guard succeeds. A firing
simplification rule <EM>replaces</EM> the head constraints by the body
constraints, a firing propagation rule keeps the head constraints and
<EM>adds</EM> the body. A firing simpagation rule keeps the first head
and replaces the second head by the body. See the next subsection for
more details.<BR>
<BR>
<A NAME="toc40"></A>
<H3 CLASS="subsection"><A NAME="htoc85">8.4.2</A>&nbsp;&nbsp;How <FONT COLOR=purple>CHR</FONT>s Work</H3>
ECL<SUP><I>i</I></SUP>PS<SUP><I>e</I></SUP> will first solve the built-in constraints, 
then user-defined constraints by <FONT COLOR=purple>CHR</FONT>s&nbsp; then the other goals.<BR>
<BR>
<B>Example, contd.:</B> <PRE CLASS="verbatim">
[eclipse]: chr(minmax).
minmax.chr compiled traceable 106874 bytes in 3.37 seconds
minmax.pl  compiled traceable 124980 bytes in 1.83 seconds
yes.
[eclipse]: minimum(X,Y,Z), maximum(X,Y,Z).
X = Y = Z = _g496
yes.
</PRE>
Each user-defined constraint is associated with all rules in whose
heads it occurs by the <FONT COLOR=purple>CHR</FONT> compiler. Every time a user-defined
constraint goal is added or re-activated, it checks itself the
applicability of its associated <FONT COLOR=purple>CHR</FONT>s by <EM>trying</EM> each <FONT COLOR=purple>CHR</FONT>. To
try a <FONT COLOR=purple>CHR</FONT>, one of its heads is matched against the constraint goal.
If a <FONT COLOR=purple>CHR</FONT> has two heads, the constraint store is searched for a
&#8220;partner&#8221; constraint that matches the other head. If the matching
succeeded, the guard is executed as a test. Otherwise the rule delays
and the next rule is tried.<BR>
<BR>
The guard<A NAME="@default236"></A> either succeeds, fails or delays. If the guard succeeds,
the rule fires. Otherwise the rule delays and the next rule is tried.
In the current implementation, a guard succeeds if its execution
succeeds without delayed goals and attempts to &#8220;touch&#8221; a global
variable (one that occurs in the heads). A variable is <EM>touched</EM>
if it is unified with a term (including other variables), if it gets
more constrained by built-in constraints (e.g. finite domains or
equations over rationals) or if a goal delays on it (see also the <TT>check_guard_bindings</TT> option<A NAME="@default237"></A>). Currently, built-in constraints used
in a guard act as tests only (see also the section on writing good
<FONT COLOR=purple>CHR</FONT> programs).<BR>
<BR>
If the firing <FONT COLOR=purple>CHR</FONT> is a simplification rule, the matched constraint
goals are removed and the body of the <FONT COLOR=purple>CHR</FONT> is executed. Similarly
for a firing simpagation rule, except that the first head is kept. If
the firing <FONT COLOR=purple>CHR</FONT> is a propagation rule the
body of the <FONT COLOR=purple>CHR</FONT> is executed and the next rule is tried. It is remembered
that the propagation rule fired, so it will not fire again (with the
same partner constraint) if the constraint goal is re-activated.<BR>
<BR>
If the constraint goal has not been removed and all rules have been tried,
it delays until a variable occurring in the constraint is touched.
Then the constraint is re-activated and all its rules are tried
again.<BR>
<BR>
<B>Example, contd.:</B>
The following trace is edited, 
rules that are tried in vain and redelay have been removed. 
<PRE CLASS="verbatim">
[eclipse]: chr_trace.
yes.
Debugger switched on - creep mode
[eclipse]: notrace.     % trace only constraints
Debugger switched off
yes.
[eclipse]: minimum(X,Y,Z), maximum(X,Y,Z).

ADD (1) minimum(X, Y, Z)
TRY (1) minimum(_g218, _g220, _g222) with propagation
RULE 'propagation' FIRED

 ADD (2) leq(_g665, _g601)

 ADD (3) leq(_g665, Var)

ADD (4) maximum(_g601, Var, _g665)
TRY (4) maximum(_g601, Var, _g665) with propagation
RULE 'propagation' FIRED

 ADD (5) leq(_g601, _g665)
 TRY (5) leq(_g601, _g665) (2) leq(_g665, _g601) with antisymmetry
 RULE 'antisymmetry' FIRED

TRY (4) maximum(_g601, Var, _g601) with max_eq
RULE 'max_eq' FIRED

 ADD (6) leq(Var, _g601)
 TRY (3) leq(_g601, Var) (6) leq(Var, _g601) with antisymmetry
 RULE 'antisymmetry' FIRED

TRY (1) minimum(_g601, _g601, _g601) with min_eq
RULE 'min_eq' FIRED

 ADD (7) leq(_g601, _g601)
 TRY (7) leq(_g601, _g601) with reflexivity
 RULE 'reflexivity' FIRED

X = Y = Z = _g558
yes.
</PRE>
<HR>
<A HREF="libman045.html"><IMG SRC ="previous_motif.gif" ALT="Previous"></A>
<A HREF="libman042.html"><IMG SRC ="contents_motif.gif" ALT="Up"></A>
<A HREF="libman047.html"><IMG SRC ="next_motif.gif" ALT="Next"></A>
</BODY>
</HTML>
